COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Universality of first order logic
C00012 ENDMK
C⊗;
Universality of first order logic

	I have been in the Far East and have just looked at the
discussion of expressibility in first order logic.  The point
I thought I was making in my original message seems to have
been mainly missed.  DAM's example of the transitive
closure of a relation provides a good example of what I meant.

	Suppose  R(x,y)  is a transitive relation.  The transitivity
is expressed by the first order formula

	(x y z)(R(x,y) & R(y,z) → R(x,z)).

In second order logic we can define the transitive closure of a relation.
We use the auxiliary second order relation  covers(R',R)  defined
by

	(R R')(covers(R',R) iff (x y)(R(x,y) → R'(x,y)))

and then define  tc(R',R)  by

	(R R')(tc(R,R') iff transitive(R') & covers(R',R)
& (R")(transitive(R") & covers(R",R) → covers(R",R'))).

This asserts that  R'  is transitive and covers  R  and is the
least relation that does so.

	Suppose we don't want to use second order logic, i.e. we
don't want to quantify over relations.  We can introduce a domain
of objects that we will call Relations, i.e. we reify (make things
out of) relations.  Relations are first order
objects.  We introduce a predicate  applies(r,x,y)  whose intended
meaning is that the Relation  r  applies to the pair  x  and  y.
We define a predicate  Transitive  by

	(r)(Transitive(r) iff (x y z)(applies(r,x,y) & applies(r,y,z)
→ applies(r,x,z))

and a predicate  Covers  by

	(r r')(Covers(r',r) iff (x)(applies(r,x,y) → applies(r',x,y))).

We write the analogous formula for the predicate  Tc  denoting
transitive closure, namely

	(r r')(Tc(r,r') iff Transitive(r') & Covers(r',r) &
(r")(Transitive(r") & Covers(r",r) → Covers(r",r'))).

	This represents our attempt to make first order objects
out of relations.  However, as DAM is no doubt ready to point out,
we haven't quite won.  There is nothing that requires that our
domain  Relations  reifies all relations.  Thus for some relation
R,  there might not exist  r  in  Relations  such that

	(x y)(applies(r,x,y) iff R(x,y)).

Therefore, our definition of  Tc(r',r)  is inadequate in that the
minimum transitive object in  Relations  covering  r  may not
correspond to the transitive closure of the relation
R  defined by

	(x y)(R(x,y) iff applies(r,x,y)).

Thus our first order theory of  Tc  is incomplete.
However, second order logic isn't such a big win either, because
second order logic itself is incomplete.  Not every formula true
in all models of second order logic is  provable in second order
logic.  This contrasts with the completeness of first order logic.
This tradeoff between incompleteness of theories and incompleteness
of the logic is unavoidable.

	Now we come to questions of strategy.  Suppose we are
interested in formalizing a robot's ability to compute certain
relations, i.e. we want to introduce a predicate
can-compute(Robby,R)  where  R  is a relation.  This is a second
order theory and (for example), not suitable for ordinary resolution
theorem proving.  An alternative is to use  Can-compute(Robby,r),
where  r  is taken from the domain of  Relations.  This may be
advantageous, especially if we are really interested in some
restricted set of binary relations.

	A rather powerful choice is to use Zermelo-Frankel
set theory.  This is a first order theory in which the objects
are sets and the one relation of the theory is  x in y.  We can
form ordered pairs and sets of ordered pairs, so relations can
be introduced as sets of ordered pairs.  Instead of  R(x,y), we
write

	(x,y) in R.

The computationally difficult part of ZF for theorem provers
is to make them use the axiom schema of comprehension and the
somewhat more difficult axiom schema of replacement.  The schema
of comprehension permits is

	(x)(Ey)(z)(z in y iff z in x & Foo),

where  Foo  is any formula with  z  as its free variable.
This allows us to form a set out of those elements of the
set  x  that have the property expressed by the formula  Foo.
Frege's original formulation allowed forming a set of those
all objects that had a property  Foo,  but Russell showed that
if you took Foo to be  not(z in z), you could quickly derive
a contradiction.  Making the computer invent properties  Foo
relevant to solving problems or deriving theorems is difficult -
even more difficult than making the computer invent suitable
instances of the axiom schema of induction in arithmetic or
Lisp theory.  Only Boyer and Moore do much with the latter, and,
to my knowledge, no-one has written a program that invents
formulas for doing comprehension.  We won't have powerful AI
until someone does.

	In the meantime it is may be worthwhile to use systems
weaker than set theory in which only certain kinds of sets
are used as objects.  Whether we do it in first or second order
logic is a question of technical convenience, but it may be
quite important in making a program practical.

	An example is the blocks world in which  above(x,y)  is
taken to be the transitive closure of  on(x,y).  If all we want
is above, we don't need anything fancy.  We simply write

	(x y)(on(x,y) → above(x,y)),

	(x y z)(above(x,y) & above(y,z) → above(x,z))

and use the schema

	(x y)(on(x,y) → P(x,y)) & (x y z)(P(x,y) & P(y,z) → P(x,z))
→ (x y)(above(x,y) → P(x,y)).

The schema is more tedious to use than the simple axioms, and
it is often unnecessary.  Specifically, if we want to prove
above(a,b)  in some case, we can usually get by with the axioms
only.  However, if we want to prove  not above(a, b)  or to
prove formulas of the form  (x y)(above(x,y) → . . .), then
we'll have to use the schema.

	However, if we want as system that might invent  above
as the transitive closure of  on,  then we need something stronger.
We are forced either make our programs use higher order logic or
to reify a domain of relations that will include those we want,
e.g. will include at least  on  and  above.

	On some other occasion, I hope to go on at greater length
and more systematically about when it is convenient to reify
various domains of entity.